#include "ComboReduct/combo/variable_unifier.h"

namespace combo{

variable_unifier& variable_unifier::DEFAULT_VU(){
	static combo::variable_unifier * vu = new combo::variable_unifier();
	return *vu;
}

variable_unifier::variable_unifier(){
	this->oneVariableActive = false;
}

variable_unifier::variable_unifier(const variable_unifier& unifier){
	this->oneVariableActive = unifier.isOneVariableActive();
	this->umap = unifier.getMap();
}

variable_unifier::~variable_unifier(){
}

const combo::UnifierMap& variable_unifier::getMap() const { 
	return this->umap;
}

UnifierIt variable_unifier::getMapBeginIterator() {
	return this->umap.begin();
}

UnifierIt variable_unifier::getMapEndIterator() {
	return this->umap.end();
}

bool variable_unifier::getVariableState(std::string& variable) {
    if(this->umap.find(variable) == this->umap.end()){
        return false;
    }
    return this->umap[variable];
}

void variable_unifier::setVariableState(std::string& variable, bool state){
    this->umap[variable] = state;
}

void variable_unifier::insert(const std::string& variable, const bool state){
	// unifier map already contains the key
	if(this->umap.find(variable) != this->umap.end()) { 
		return; 
	}
	
	this->umap.insert(std::pair<std::string, bool>(variable, state));
}

bool variable_unifier::contains(const std::string& variable) const {
    return (this->umap.find(variable) != this->umap.end());
}

int variable_unifier::mapSize() const {
    return this->umap.size();
}

void variable_unifier::unify(combo::UnifierOperation operation, 
							 variable_unifier& unifier){
	
	// no need to unify empty maps - this should be the default
	if(isEmpty() && unifier.isEmpty()){ return; }
	
	if(mapSize() != unifier.mapSize()){
		// error
		return;
	}
	
	// reset oneVariableActive state befor unification starts
	this->oneVariableActive = false;
	
	UnifierIt it;
	UnifierIt otherIt;

	for(it = this->umap.begin(), otherIt = unifier.getMapBeginIterator(); 
		it != this->umap.end() && otherIt != unifier.getMapEndIterator(); it++, otherIt++){
		
		if(it->first != otherIt->first){
			// log
			continue;
			
		} else {
			
			// and unification, just AND the states of the variables
			if(operation == combo::UNIFY_AND){
				it->second = (it->second && otherIt->second);
				
				if(it->second){
					this->oneVariableActive = true;
				}
				
			// not / or unification, XOR the states of the variables
			} else if(operation == combo::UNIFY_OR  || 
					  operation == combo::UNIFY_NOT ){
				it->second = (it->second ^ otherIt->second);
				
				if(it->second){
					this->oneVariableActive = true;
				}
			}			
		}
	}	
}

} // namespace combo
